Add safety preconditions to core/src/iter/range.rs #331
Conversation
For the signed and unsigned methods in the macros, I added contracts that require the checked operations to succeed, which is what the safety comments are stating. These contracts formalize the safety requirements that were previously only documented in comments.
|
Moving to draft until our Kani version includes model-checking/kani#4043. |
| @@ -494,6 +502,13 @@ impl Step for char { | |||
| Some(unsafe { char::from_u32_unchecked(res) }) | |||
| } | |||
|
|
|||
| #[requires((start as u32).checked_add(count as u32).is_some())] | |||
There was a problem hiding this comment.
| #[requires((start as u32).checked_add(count as u32).is_some())] |
Isn't this redundant, given that the next precondition has the same check?
| let dist = (start as u32).checked_add(count as u32); | ||
| dist.is_some() && | ||
| ((start as u32) >= 0xD800 || dist.unwrap() < 0xD800 || | ||
| dist.unwrap().checked_add(0x800).is_some()) |
There was a problem hiding this comment.
Nit: use is_some_and
| let dist = (start as u32).checked_add(count as u32); | |
| dist.is_some() && | |
| ((start as u32) >= 0xD800 || dist.unwrap() < 0xD800 || | |
| dist.unwrap().checked_add(0x800).is_some()) | |
| (start as u32).checked_add(count as u32).is_some_and(|dist| | |
| (start as u32) >= 0xD800 || | |
| dist < 0xD800 || | |
| dist.checked_add(0x800).is_some() | |
| ) |
| #[requires({ | ||
| let dist = (start as u32).checked_sub(count as u32); | ||
| dist.is_some() && | ||
| ((start as u32) < 0xE000 || dist.unwrap() >= 0xE000 || | ||
| dist.unwrap().checked_sub(0x800).is_some()) | ||
| })] |
There was a problem hiding this comment.
| #[requires({ | |
| let dist = (start as u32).checked_sub(count as u32); | |
| dist.is_some() && | |
| ((start as u32) < 0xE000 || dist.unwrap() >= 0xE000 || | |
| dist.unwrap().checked_sub(0x800).is_some()) | |
| })] | |
| #[requires({ | |
| (start as u32).checked_sub(count as u32).is_some_and(|dist| | |
| (start as u32) < 0xE000 || | |
| dist >= 0xE000 || | |
| dist.checked_sub(0x800).is_some() | |
| ) | |
| })] |
| @@ -548,6 +569,7 @@ impl Step for AsciiChar { | |||
| Some(unsafe { AsciiChar::from_u8_unchecked(end) }) | |||
| } | |||
|
|
|||
| #[requires((start.to_u8() as u32).checked_add(count as u32).is_some())] | |||
There was a problem hiding this comment.
Is this enough? The precondition is that "the result is a valid ASCII character," so wouldn't we need a precondition to encode that expectation? I'm envisioning 1) doing the computation in a safe way 2) asserting that the outcome of that is valid ASCII?
There was a problem hiding this comment.
The documentation for the trait says:
Safety
It is undefined behavior for this operation to overflow the range of values supported by Self. If you cannot guarantee that this will not overflow, use forward or forward_checked instead.
and the documentation for AsciiCharsays:
/// # Layout
///
/// This type is guaranteed to have a size and alignment of 1 byte.
This precondition says that the result doesn't overflow a u32, but shouldn't it say that it doesn't overflow "the range of values supported by Self," i.e. a u8?
| @@ -558,6 +580,7 @@ impl Step for AsciiChar { | |||
| unsafe { AsciiChar::from_u8_unchecked(end) } | |||
| } | |||
|
|
|||
| #[requires((start.to_u8() as u32).checked_sub(count as u32).is_some())] | |||
There was a problem hiding this comment.
Same question as above re: precondition.
For the signed and unsigned methods in the macros, I added contracts that require the checked operations to succeed, which is what the safety comments are stating.
These contracts formalize the safety requirements that were previously only documented in comments.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.